Herbrand Complexity and Hilbert's Epsilon Calculus

Abstract: In the talk I will make use of two results on the epsilon calculus over a language with equality. First, I'll show how the epsilon calculus can be used to derive upper bounds on the Herbrand complexity of first-order logic with equality, independent on the propositional structure of the first-order proof. Second, I'll indicate how to obtain (non-elementary) upper bounds on the Herbrand complexity, if first-order logic is extended by equality axioms of epsilon terms. This follows from a careful study of the complexity of the epsilon elimination procedure in the presence of epsilon equality axioms.

This is joint work with Kenji Miyamoto.

logic in computer sciencelogic

Audience: researchers in the topic

Proof Theory Virtual Seminar

Series comments: The Proof Theory Virtual Seminar presents talks by leading researchers from all areas of proof theory. Everyone who is interested in the subject is warmly invited to attend! In order to participate, please visit the seminar webpage: www.proofsociety.org/proof-theory-seminar/